E:Type, T,V:(IdIdType), M:(IdLnkIdType), pred?:(E(?E)), info:(E((:Id  Id) + (:(:IdLnk
E:Type, T,V:(IdIdType), M:(IdLnkIdType), pred?:(E(?E)), info:(E( E)  Id))),
init:(i:IdEState((T(i)))), Trans:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))
init:(i:IdEState((T(i)))), Trans:(EState((T(i)))EState((T(i)))),
val:(e:Ekindcase(kind(e); a.(V(loc(e),a)); l,t.(M(l,t)))), time:(Erationals).
(e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 SWellFounded(pred!(e;e'))
 (e:E. state_when(e)  EState((T(loc(e))))) 

latex

Definitions	t  T, Id, x:A. B(x), loc(e), f(a), EState(T), x.A(x), x. t(x), t.1, x:A  B(x), P  Q, when-after(e;info;pred?;init;Trans;val;time), x:AB(x), s = t, state_when(e), Type, IdLnk, Unit, left + right, x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t)), Knd, kind(e), rationals, pred(e), prop{i:l}, first(e), b, A, pred!(e;e'), SWellFounded(R(x;y))
Lemmas	strongwellfounded wf, pred! wf, not wf, assert wf, first wf, pred wf, rationals wf, kind wf, Knd wf, kindcase wf, unit wf, IdLnk wf, when-after wf, pi1 wf, EState wf, loc wf, Id wf